| Definitions |  x:A. B(x), P   Q, P & Q, Prop, t  T,   x. t(x), {T}, event-info(ds;da), Top, S  T, P  Q, P Q,  T, True, let x,y,z = a in t(x;y;z), A & B, P  Q, SQType(T),  , A B,  A, False, l1 || l2, i j,  b, null(as), true, false, if b t else f fi, concat(ll), reduce(f;k;as), Y, ||as||, ecl-halt(ds;da;x), x(s),  x:A. B(x), Valtype(da;k), as @ bs, l1 l2, xL. P(x), Dec(P), star-append(T;P;Q), (xL.P(x)) |
| Lemmas | ecl-induction, event-info wf, nat wf, ecl-halt wf, compat wf, guard wf, ecl wf, eclbase wf, decl-state wf, ma-valtype wf, bool wf, eclseq wf, ecland wf, eclor wf, eclrepeat wf, eclact wf, eclthrow wf, eclcatch wf, fpf wf, Knd wf, Id wf, length wf1, non neg length, member wf, compat-append, fpf-cap wf, Kind-deq wf, top wf, append nil sq, append wf, compat-append2, compat-cons, squash wf, true wf, append assoc, member append, or functionality wrt iff, l member wf, cons member, not wf, assert wf, Knd sq, subtype rel self, iseg append0, iseg wf, le wf, common iseg compat, iseg transitivity, iseg weakening, decidable lt, compat-iseg, compat symmetry, iseg antisymmetry, concat wf, l all wf, nat properties, ge wf, l all cons, false wf, iseg append, length-append, ecl-halt-nil |
Type, da:k:Knd fp
}